COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	
C00009 00003	.BIB
C00014 ENDMK
C⊗;

John--this is an update of what I wrote in the ARPA proposal; it was slanted 
towards Program Verification. 
I would want to say more about special purpose proof procedures
for different kinds of domains of reasoning, building strategy
selection into representation of facts in the domains.
There are also questions of reasoning in inconsistent models of
domains, minimal changes in plans that dont quite work at runtime,
and many other things on Pattes blackboard.


.sss Details of the Theorem-prover

.cb Features
1.  Input-output is in natural mathematical notation.

2.  Based on resolution and other inference rules.

3.  Contains many search and goal reduction strategies.

4.  Has a user interface language for describing strategies
and guiding proof searches. [4]

5. Has an proof analysis method for extracting answers to
questions from proofs. This is intended for question-answering
applications.

.cb Achievements

1.   Proofs  of many  research results  (announced  without proof  in
Notices  Amer. Math. Soc.)  were obtained  over the last  five years.
These include announced theorems  in such topics as Boolean  Algebra,
Lattice Theory,  Group Theory  and Geometry.   In some  cases we were
able to mail the machine proofs to the authors before the authors had
written up  their own  proofs, and  in other  cases modifications  or
extensions of  the results were  found. The total  number of theorems
and subsidiary lemmas involved is on the order of fifty; the
main references are [5,6] and a forthcoming report.

2.  Verification of complex sorting programs from first principles [5].

3. Has recently been used by Stan Tarnlund to write about 10 programs
(include tree searching and sorting algorithms)
according to Kowalski's theory of the use of Predicate Calculus as a 
programming language.


General Status of Theorem Proving Field.

Very strong theorem proving programs now exist at Argonne Labs. (assembly
language coded for IBM 370 series; very fast on complicated Algebra examples,
has found a few 100-Resolution-step proofs in 1 minute cpu time; not very
flexible in changing sets of stategies nor for interactive use.),
 Austin, Texas (highly interactive,
applicable to checking of proofs in Topology and Real variable Theory),
and Stanford A.I.Lab (features above). 
These programs represent very good progress towards the automation of 
basic first order reasoning. Emphasis seems now to be needed on various
forms of the representation problem: representation of the problem to be
solved, of likely methods of solution (both likely and method or strategy)
and analogy (e.g analogous problem and solution).
Interactive use of these programs has been shown (Stanford and Texas) to
be the most promising direction towards useful applications, and here the 
problem of design of descriptive languages for incomplete reasoning (to be
filled in automatically)  must be tackled.

.cb Proposals

1.  Implementation of new proof rules and strategies  (start Jan.1975).
Many special purpose proof search methods can be programmed in terms of
restricted resolution search strategies. So such extensions are not difficult
to do.
The objective here is to speed up the prover on specific problem domains
that arise in areas of mathematics, everyday discourse, and
program verification.  This will involve testing the prover
on many of the experimental goals of the verification system (September 1976).

2.  Interface with the Verifier.
The present interface is rudimentary.  We want to use the prover as a subsystem
of the verifier, and have the ability to switch back and forth between the
two with data and problems.  This requires a more sophisticated interface. (June
1976).

3. HUNCH language.
Future usability and applications of the theorem prover depend heavily on
the strategy language.  The present language is a nucleus which must be
extended into a facility which enables the user to program outlines of proofs
(i.e. a proof search programming language).  The nature of such languages
is largely unexplored and we expect this to be the most important development
for the prover.

.BIB
⊗  N. Suzuki, "Verifying Programs by Algebraic and Logical Reduction",
AIM-255, December 1974; (accepted for the 1975 <International Conference
on Reliable Software>, Los Angeles April 22-24, 1975).

⊗  F.W.v. Henke and D.C. Luckham, "A Methodology for Verifying Programs",
A.I.Memo forthcoming; (accepted for the 1975 <International Conference
on Reliable Software>, Los Angeles, April 22-24, 1975).

⊗  N. Suzuki, "Short Users Manual for the Stanford Pascal Program Verifier",
Stanford A. I. Lab. Operating Note (forthcoming); diskfile: VCG.MAN [MAN,SUZ]
@SAIL.

⊗  J.R. Allen, "Preliminary  Users   Manual   for   an   Interative
Theorem-Prover",  Stanford   Artificial   Intelligence   Laboratory
Operating Note SAILON-73.

⊗  Jorge J. Morales,  "Interactive Theorem Proving", <Proc. ACM National
Conference>,  August 1973,  pp.441; also "Report on the 
Verification of Sorting Programs", (forthcoming), available as SORTED.EX
[1,JJM] at SAIL.

⊗  John  Allen  and  David Luckham,   "An  Interactive  Theorem-proving
Program", <Proc.   Fifth International  Machine Intelligence
Workshop>, Edinburgh University Press, Edinburgh, 1970.

⊗  S. Igarashi, R. London,   D. Luckham, "Automatic   Program
Verification  I,  Logical  Basis  and  Its Implementation",
AIM-200, May 1970; to appear in <Acta Informatica>.

⊗  David  Luckham  and  Jack  Buchanan,  "Automatic Generation of
Programs  Containing Conditional Statements", <Proc.
A.I.S.B. Summer Conference,> Sussex, England, July 1974, pp.102-126.

⊗  Jack Buchanan and David Luckham, "On Automating the Construction of Programs",
AIM-236, May 1974; (submitted to the <JACM>).

⊗  J.R. Buchanan, "A Study in Automatic Programming", <Ph.D. Thesis>, AIM-245,
July 1974.

⊗  Per Brinch Hansen, "The Purpose of Concurrent Pascal", invited paper,
 <International Conference on Reliable Software>, Los Angeles, April 22-24, 1975).

⊗  R. Balzer, T.E. Cheatham, S. Crocker, "Design of a National Software Works",
report ISI-RR-73-16.

⊗  C.A.R. Hoare, "Proof of a program: FIND", Comm. ACM 14, Jan. 1971, pp.39-45.

⊗  R.W. Floyd, "Algorithm 245 TREESORT3", Comm.ACM. 13, June 1970, pp.371-373.

⊗ D. Knuth, "The Art of Computer Programming Vol.3- Sorting and Searching",
Addison-Wesley, Reading, Mass. 1973.

⊗  V. Pratt, "Shell Sort and Sorting Networks", Ph.D. Thesis, Stanford Un. 
Feb. 1972.

⊗  C.A.R. Hoare, "A Structural Approach to Protection", Computer Science
Dept., Queen's University of Belfast, Draft Jan. 1975.

⊗  W.A. Wulf, "ALPHARD: Toward a Language to Support Structured Programs",
Carnegie Mellon University, Report April 1974.

.end